$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$$B$), $L$:$A$ List, $L_{1}$, $L_{2}$:$B$ List.
\\[0ex]map($f$;$L$) $=$ ($L_{1}$ @ $L_{2}$) $\in$ $B$ List
\\[0ex]$\Rightarrow$ \{map($f$;firstn($\parallel$$L_{1}$$\parallel$;$L$)) $=$ $L_{1}$ \& map($f$;nth\_tl($\parallel$$L_{1}$$\parallel$;$L$)) $=$ $L_{2}$\}